A:Type, B:(AType), eq:EqDecider(A), f, g:a:A fp B(a). g  f  f || g 

latex

Definitions	x:A. B(x), x(s), P  Q, f  g, f || g, A c B, P & Q, t  T, , x. t(x)
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, fpf wf, deq wf